; <!-- 4 -->
; <lemma>
;  <title></title>
;  <origin>BepiColombo_Models_V3.3 | csw_C0 | thm15/THM</origin>
;  <theories>
;    <theory name="linear_order_int"/>
;    <theory name="basic_set"/>
;  </theories>
;  <typenv>
;    <variable name="TC_SERVICES" type="POW(INT)"/>
;  </typenv>
;  <hypothesis needed="true">TC_SERVICES={3,6,9,17,21,200,201,202,203}</hypothesis>
;  <goal>! k . k : TC_SERVICES => k >= 0 & k <= 255</goal>
;	<goal>∀ k · k∈TC_SERVICES ⇒ k≥0 ∧ k≤255</goal> 
; </lemma>

(benchmark bepi_colombo_thm15
  :logic AUFLIA
  :extrapreds ((TC_SERVICES Int))
  :extramacros ((enum1 
		  (lambda (?s Int) . 
		     (or
		       (= ?s 3) 
		       (= ?s 6)
		       (= ?s 9)
		       (= ?s 17)
		       (= ?s 21)
		       (= ?s 200)
		       (= ?s 201)
		       (= ?s 202)
		       (= ?s 203)
		       )))
		 (in (lambda (?e 't) (?p ('t boolean)) . (?p ?e)))
		 )
  :assumption (= TC_SERVICES enum1)
  :formula
  (not
    (forall (?k Int)
      (implies 
	(in ?k TC_SERVICES)
	(and (>= ?k 0)
	  (<= ?k 255))))
    )
)
    